Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	eq(0,0)	→ true
2:	eq(0,s(m))	→ false
3:	eq(s(n),0)	→ false
4:	eq(s(n),s(m))	→ eq(n,m)
5:	le(0,m)	→ true
6:	le(s(n),0)	→ false
7:	le(s(n),s(m))	→ le(n,m)
8:	min(cons(0,nil))	→ 0
9:	min(cons(s(n),nil))	→ s(n)
10:	min(cons(n,cons(m,x)))	→ if_min(le(n,m),cons(n,cons(m,x)))
11:	if_min(true,cons(n,cons(m,x)))	→ min(cons(n,x))
12:	if_min(false,cons(n,cons(m,x)))	→ min(cons(m,x))
13:	replace(n,m,nil)	→ nil
14:	replace(n,m,cons(k,x))	→ if_replace(eq(n,k),n,m,cons(k,x))
15:	if_replace(true,n,m,cons(k,x))	→ cons(m,x)
16:	if_replace(false,n,m,cons(k,x))	→ cons(k,replace(n,m,x))
17:	sort(nil)	→ nil
18:	sort(cons(n,x))	→ cons(min(cons(n,x)),sort(replace(min(cons(n,x)),n,x)))

There are 12 dependency pairs:

The approximated dependency graph contains 5 SCCs: {19}, {20}, {21,23,24}, {25,27} and {28}.

Consider the SCC {19}. There are no usable rules. By taking the AF π with π(EQ) = 1 together with the lexicographic path order with empty precedence, rule 19 is strictly decreasing.

Consider the SCC {20}. There are no usable rules. By taking the AF π with π(LE) = 1 together with the lexicographic path order with empty precedence, rule 20 is strictly decreasing.

Consider the SCC {21,23,24}. The usable rules are {5-7}. By taking the AF π with π(MIN) = 1, π(IF_MIN) = 2, π(le) = [ ] and π(cons) = [2] together with the lexicographic path order with precedence le ≻ false and le ≻ true, the rules in {7,21} are weakly decreasing and the rules in {5,6,23,24} are strictly decreasing.

Consider the SCC {25,27}. The usable rules are {1-4}. By taking the AF π with π(REPLACE) = 3, π(IF_REPLACE) = 4, π(eq) = [ ] and π(cons) = [2] together with the lexicographic path order with precedence eq ≻ false and eq ≻ true, the rules in {4,25} are weakly decreasing and the rules in {1-3,27} are strictly decreasing.

Consider the SCC {28}. The usable rules are {1-16}. By taking the AF π with π(min) = π(SORT) = 1, π(if_min) = 2, π(replace) = 3, π(if_replace) = 4, π(eq) = π(le) = π(s) = [ ] and π(cons) = [2] together with the lexicographic path order with precedence eq ≻ false, eq ≻ true, le ≻ false, le ≻ true, nil ≻ 0 and nil ≻ s, the rules in {4,7,10,13-16} are weakly decreasing and the rules in {1-3,5,6,8,9,11,12,28} are strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (2.11 seconds) --- May 4, 2006